Skip to content

[Merged by Bors] - feat: rangeSplitting f is strictly monotone when f is monotone#39797

Closed
vihdzp wants to merge 1 commit into
leanprover-community:masterfrom
vihdzp:rangesplit
Closed

[Merged by Bors] - feat: rangeSplitting f is strictly monotone when f is monotone#39797
vihdzp wants to merge 1 commit into
leanprover-community:masterfrom
vihdzp:rangesplit

Conversation

@vihdzp

@vihdzp vihdzp commented May 25, 2026

Copy link
Copy Markdown
Collaborator

Open in Gitpod

@vihdzp vihdzp added easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory labels May 25, 2026
@github-actions

github-actions Bot commented May 25, 2026

Copy link
Copy Markdown

PR summary eea6c417da

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ rangeSplitting_strictMono

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-data Data (lists, quotients, numbers, etc) label May 25, 2026
@vihdzp vihdzp mentioned this pull request May 28, 2026
Closed
1 task
YaelDillies
YaelDillies approved these changes May 28, 2026
View reviewed changes

@YaelDillies YaelDillies left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! 🚀

maintainer merge

@github-actions

github-actions Bot commented May 28, 2026

Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 28, 2026
@ADedecker

ADedecker commented May 28, 2026

Copy link
Copy Markdown
Member

Thanks!

bors merge

@mathlib-triage mathlib-triage Bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 28, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 28, 2026
@vihdzp
feat: rangeSplitting f is strictly monotone when f is monotone (#…
ae7637b 
…39797)
@mathlib-bors

mathlib-bors Bot commented May 28, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat: rangeSplitting f is strictly monotone when f is monotone [Merged by Bors] - feat: rangeSplitting f is strictly monotone when f is monotone May 28, 2026
@mathlib-bors mathlib-bors Bot closed this May 28, 2026
grunweg pushed a commit to grunweg/mathlib4 that referenced this pull request May 30, 2026
@vihdzp @grunweg
feat: rangeSplitting f is strictly monotone when f is monotone (l…
da85372 
…eanprover-community#39797)
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@vihdzp @b-mehta
feat: rangeSplitting f is strictly monotone when f is monotone (l…
9072be5 
…eanprover-community#39797)
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@vihdzp @Bergschaf
feat: rangeSplitting f is strictly monotone when f is monotone (l…
5d3a9cd 
…eanprover-community#39797)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes
+1 more reviewer
@Hagb Hagb Hagb approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc) t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@vihdzp @ADedecker @Hagb @YaelDillies